RecursiveRecordNeedsInductionDeclaration.agda:4,8-9
Recursive record R needs to be declared as either inductive or coinductive
